例句與用法

1. a widely used method for checking real-time systems is, according to the real-time property to be checked, to use a proper bi-simulation equivalence relation to convert the infinite-timed state space to a finite equivalence class space . the algorithm needs only to explore the finite space to get a correct answer . in most cases, exhaustive exploration is very difficult because the equivalence class space increases explosively when the scale of the system increases . in this paper, an equivalence relation is introduced to check whether a concurrent system, which is composed of a finite set of real-time automata, satisfies a linear duration property . to avoid exhaustive exploration, this paper also introduces a compatibility relation between timed states ( configurations ) . based on these two relations, an algorithm is proposed to check whether a real-time automaton network satisfies a linear duration property . the cases study shows that under some conditions this algorithm has better efficiency than the tools in the literature
   一個被廣泛用于驗證實時系統(tǒng)的方法是根據(jù)被驗證的實時性質(zhì),使用適當?shù)碾p向模擬等價關(guān)系使無限的狀態(tài)空間轉(zhuǎn)化為有限的狀態(tài)等價類空間.算法只需要在這個有限的等價類空間里搜索就可以得到正確答案.但是,這個等價類空間的規(guī)模一般隨著系統(tǒng)規(guī)模的增大而產(chǎn)生爆炸性的增長,以至于在很多情況下,窮盡搜索這個空間是不現(xiàn)實的.該文引入了一個等價關(guān)系來驗證一個由多個實時自動機通過共享變量組成的并發(fā)系統(tǒng)是否滿足一個線性時段特性.同時，還引入了格局之間的兼容關(guān)系來避免對狀態(tài)等價類空間的窮盡搜索.基于這兩個關(guān)系,文章提出了一個算法來驗證是否一個實時自動機網(wǎng)滿足一個線性時段特性.實例研究顯示,此算法在某些情況下比其他一些工具有更好的時間和空間效率